Nuprl Lemma : atom-free-IdLnk
0,22
postcript
pdf
l
:IdLnk. AtomFree(IdLnk;
l
)
latex
Definitions
Id
,
<
a
,
b
>
,
x
.
A
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
AtomFree(
T
;
x
)
,
IdLnk
Lemmas
atom-free-Id
,
Id
wf
origin
l:IdLnk. AtomFree(IdLnk;l) l:IdLnk. AtomFree(IdLnk;l) 
x.A(x)
Tx:A. B(x)
B(x)